$\forall$$A$, $C$, $B$:Type, ${\it eqa}$:EqDecider($A$), ${\it eqc}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ $B$, $a$:$A$, $z$:$B$.
\\[0ex]Inj($A$;$C$;$r$) $\Rightarrow$ (rename($r$;$f$)($r$($a$))?$z$ = $f$($a$)?$z$ $\in$ $B$)